COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	\magnify{1100}
C00017 ENDMK
C⊗;
\magnify{1100}
\def\xskip{\hskip7pt plus3pt minus4pt}
\chcode`|=13
\def|#1|{\hbox{\it#1\/}}
\def\IF{\mathop{\bf if}}
\def\THEN{\mathrel{\bf then}}
\def\ELSE{\mathrel{\bf else}}

\ctrline{\bf CS 206---Recursive Programming and Proving}
\vskip 20pt
\ctrline{Recursive Functions and Fixpoints}
\ctrline{November 2, 1982}
\vskip 10pt
\ctrline{This handout summarizes what was presented in class on Thursday, October 28.}
\vskip 20pt

\font\tensyb=cmbsy
\def\bbot{\hbox{\tensyb\char'20}}

Our aim is to have a mathematical theory that will take programs like
$$|fact|[n]←\IF n=0\THEN 1\ELSE n\cdot|fact|[n-1]$$
and produce statements in first-order logic that describe the function |fact|.
We will do this based on the idea of a {\sl partial order}.  Recall that
a binary relation $\sqsub$ is a partial order if it is reflexive ($a\sqsub a$),
antisymmetric ($a\sqsub b$ and $b\sqsub a$ iff $a=b$), and transitive
(if $a\sqsub b$ and $b\sqsub c$, then $a\sqsub c$).  It is not necessary
that either $a\sqsub b$ or $b\sqsub a$ hold for arbitrary $a$ and $b$.
In the case that either $a\sqsub b$ or $b\sqsub a$ for every $a$ and $b$,
the relation $\sqsub$ is called a {\sl total\/} (or {\sl linear\/}) order.

Given a domain $D$, such as the natural numbers or the set of all S-expressions,
we form an {\sl extended\/} domain $D↑+$ by adding a new element, which we will
call $\bot$.  We then define the order $\sqsub$ on $D↑+$ by saying that
$a\sqsub b$ iff $a=b$ or $a=\bot$.  Thus, the extension of the natural numbers
looks like this:
$$\vbox{\hbox{$0\quad 1\quad 2\quad 3\quad \ldots$}
\vskip 15pt
\hbox{\quad\quad\quad$\bot$}}$$
If we interpret $\bot$ as ``undefined,'' then $a\sqsub b$ means ``$a$ is
less-defined than, or equal to, $b$.''  You should check that this $\sqsub$ has
all of the properties that we need for a partial ordering.

Now, another general definition.  If $A$ is a domain ordered by $\sqsub↓A$,
and $B$ is a domain ordered by $\sqsub↓B$, and $f$ and $g$ are functions
from $A$ into $B$, then we say that $f\sqsub g$ iff for all $x\in A$,
$f(x)\sqsub↓B g(x)$.  This is a natural way to order the functions from $A$ to
$B$.  Again, you should check that this satisfies the definition of an ordering.
We will assume that all of our domains have a $\bot$ element, so we can
define the function $\bbot$ by $\bbot(x)=\bot↓B$ for all $x\in A$.  This satisfies
the relation $\bbot\sqsub f$ for every function $f$ from $A$ to $B$.
In general, we will omit the subscripts indicating the domain from $\sqsub$ and
$\bot$ when the domain is apparent.

We are not interested in all of the functions from $A$ to $B$; only in those
satisfying certain properties.  One of these is {\sl monotonicity}.  A function
$f$ is monotonic if, whenever $a\sqsub b$, we have $f(a)\sqsub f(b)$.  This can
be extended to functions of several variables; $f(x↓1,\ldots,x↓n)$ is monotonic
if, whenever $a↓1\sqsub b↓1,\ldots,a↓n\sqsub b↓n$, we have
$f(a↓1,\ldots,a↓n)\sqsub f(b↓1,\ldots,b↓n)$.  Another property of functions
is that of being {\sl strict}.  This means simply that $f(\bot)=\bot$.  Or, in
the case of several arguments, $f(a↓1,\ldots,\bot,\ldots,a↓n)=\bot$.  Every
strict function is monotonic.

If we take our basic functions on numbers and S-expressions, such as the
arithmetic functions, |car|, |cdr|, and |cons|, and extend them to return $\bot$
whenever any argument is $\bot$, then they are strict and hence monotonic.
If we consider predicates as functions returning values in the domain
$\{|true|, |false|, \bot\}$, and extend |and|, |or|, |not| and
|if|--|then|--|else| appropriately, then these are also monotonic (although
not strict---for example $|or|[|true|,\bot]=|true|$).

Now let us consider functions on functions.  These are often called {\sl
functionals}.  If $\tau$ is a functional, then we might have $\tau[f]=g$,
where $f$ and $g$ are themselves functions from $A$ to $B$.  Since $A→B$
is an ordered domain, as shown above, it makes sense to talk about whether
$\tau$ is monotonic.  A particular case is the program above; from it we can
define a functional $\tau$ as follows:
$$\tau[f]=λn.\,\IF n=0\THEN 1\ELSE n\cdot f(n-1).$$
This functional $\tau$ is formed by composing functions that we know to be
monotonic; therefore, by a theorem not proved here, we can state that $\tau$
is monotonic.  We can also now write our program in the form
$$|fact|(n)←\tau[|fact|](n).$$

The only particular function we have dealt with so far is $\bbot$, the totally
undefined function.\xskip (We are using the natural numbers, extended with
$\bot$, as both $A$ and $B$ here.)\xskip
Let us see what happens if we apply $\tau$ to $\bbot$.
$$\eqalign{\tau[\bbot]&\null=λn.\,\IF n=0\THEN 1\ELSE n\cdot\bbot(n-1)\cr
&\null=λn.\,\IF n=0\THEN 1\ELSE n\cdot\bot\cr
&\null=λn.\,\IF n=0\THEN 1\ELSE \bot\cr}$$
The result is a function defined only at 0, but this is progress.  If we now
take $\tau[\tau[\bbot]]$, we will get
$$\tau[\tau[\bbot]]=λn.\,\IF n=0\THEN 1\ELSE\IF n=1\THEN 1\ELSE\bot.$$
Continuing this way, we can see that for each natural number $i$, 
$$\tau↑i[\bbot]=λn.\,\IF n<i\THEN n!\ELSE\bot.$$
(We can see this, though we haven't proved it formally.)  Thus, if we take the
``limit'' of this sequence $\tau↑i[\bbot]$ of functions, we will get the
factorial function that we originally wrote a program to compute.

Let us analyze the situation a bit further.  It is easy to prove that
$\bbot\sqsub\tau[\bbot]$.  Then, since $\tau$ is monotonic, we can apply
$\tau$ to each side of this relation and get $\tau[\bbot]\sqsub\tau[\tau[\bbot]]$.
We can continue this and write
$$\bbot\sqsub\tau[\bbot]\sqsub\tau[\tau[\bbot]]\sqsub\cdots
\sqsub\tau↑i[\bbot]\sqsub\tau↑{i+1}[\bbot]\sqsub\cdots.$$
We say that an ordered domain is {\sl complete\/} if an infinite sequence
$a↓0\sqsub a↓1\sqsub\cdots\sqsub a↓i\sqsub\cdots$ always has a ``limit
point'' $a$ in the domain.  All of the domains we will deal with are
complete, and the limit is the {\sl least upper bound\/} (lub) of the
sequence, i.e., each $a↓i\sqsub a$, and for any $b$ in the domain, if all
$a↓i\sqsub b$, then $a\sqsub b$.  So we know that the sequence $\tau↑i[f]$ has
a limit, which we will call $f$, but it wouldn't be interesting (in fact,
it would be quite discouraging) unless this function $f$ was, in fact, the
factorial function.

To prove this, we first make another definition.  We say that a function
$g$ is {\sl continuous\/} if, whenever $x↓i→x$ (i.e., $x$ is the limit of
the sequence $x↓i$), then $g(x↓i)→g(x)$.  And, we state without proof the
fact that a functional built by the composition of monotonic functions is
continuous.  So, $\tau$ is continuous.  Now, consider the sequence
$\tau↑i[\bbot]$, which has $f$ as its limit.  By the result just stated, we
know that if we apply $\tau$ to each element of this sequence, the resulting
sequence will have $\tau[f]$ as its limit.  But applying $\tau$ to the
sequence $\tau↑i[\bbot]$ produces the sequence $\tau↑{i+1}[\bbot]$, which
has the same limit as the original sequence, namely $f$.  Thus we have shown
that $\tau[f]=f$, which is expressed by saying that $f$ is a {\sl fixed point\/}
of $\tau$.  In fact, we can go on to show that $f$ is the {\sl least\/}
fixed point of
$\tau$, i.e., that $f\sqsub g$ for any fixed point of $\tau$.  Recapitulating,
the limit of the sequence $\tau↑i[\bbot]$, when $\tau$ is continuous, is the
least fixed point of $\tau$.

But it is also easy to show that the factorial function is the least fixed point
of $\tau$, and that the least fixed point is unique.  We have yet to make a
statement about what function |fact| is defined by the program
$$|fact|(n)←\tau[|fact|](n),$$
but the obvious choice is that |fact| is the least fixed point of $\tau$.

So what have we gained?  We could have simply written
$$∀n.\,fact(n)=\IF n=0\THEN 1\ELSE n\cdot|fact|(n-1),$$
which is another way of saying $|fact|=\tau[|fact|]$, and everything would
work.  Where we gain something is with programs that may not terminate for
all arguments.  For example, let
$$|loop|(n)←|loop|(n)+1.$$
Saying that $∀n.\,|loop|(n)=|loop|(n)+1$ is deadly, since from it we can
prove false statements like $0=1$.
However, if we let $\tau[f]=λn.\,f(n)+1$, and then let
|loop| be the least fixed point of $\tau$, which is the limit of the sequence
$\tau↑i[\bbot]$, we get something useful, since for all $i$, $\tau↑i[\bbot]=\bbot$
and therefore $|loop|=\bbot$.  Stated another way, $∀n.\,|loop|(n)=\bot$, and,
since $\bot+1=\bot$, we have no contradictions.

\vskip 20pt
\parindent 0pt
\parskip 6pt

References:

[1] Manna, Z.\quad {\sl Mathematical Theory of Computation}, McGraw-Hill, 1974.
Chapter 5 contains a complete introduction to this subject.

[2] Stoy, J. E.\quad {\sl Denotational Semantics: The Scott-Strachey Approach
to Programming Language Theory}, MIT Press, 1977.  This is a more advanced book
that develops all the details of this theory and applies it to the semantics
of programming languages.

\vfill\end